\begin{tabbing}
1. $T$ : Type
\\[0ex]2. $T$ List
\\[0ex]3. $u$ : $T$
\\[0ex]4. $v$ : $T$ List
\\[0ex]5. \=$\forall$$x$, $y$:$T$.\+
\\[0ex]no\_repeats($T$;$v$)
\\[0ex]$\Rightarrow$ adjacent($T$;$v$;$x$;$y$)
\\[0ex]$\Rightarrow$ ($\forall$$z$:$T$. $z$ before $y$ $\in$ $v$ $\Rightarrow$ ($z$ before $x$ $\in$ $v$ $\vee$ ($z$ = $x$)))
\-\\[0ex]6. $x$ : $T$
\\[0ex]7. $y$ : $T$
\\[0ex]8. no\_repeats($T$;$v$)
\\[0ex]9. $\neg$($u$ $\in$ $v$)
\\[0ex]10. 0 $<$ $\parallel$$v$$\parallel$
\\[0ex]11. adjacent($T$;$v$;$x$;$y$)
\\[0ex]12. $z$ : $T$
\\[0ex]13. $z$ = $u$
\\[0ex]14. ($y$ $\in$ $v$)
\\[0ex]15. $\forall$$z$:$T$. $z$ before $y$ $\in$ $v$ $\Rightarrow$ ($z$ before $x$ $\in$ $v$ $\vee$ ($z$ = $x$))
\\[0ex]$\vdash$  $z$ before $x$ $\in$ [$u$ / $v$]
\end{tabbing}